﻿module sparseMatrix

type DataFlow = (int * int * AbstractDomain.abstractValue * Pattern.Pat)
type matrix = M of (DataFlow) list
        (* meaning: a SORTED list of entries (i,j,value)
        the sorting order is (j,i) to keep columns together *)

let lstPrt(M m) = List.map (fun (i,j,v,p) -> (i, j, AbstractDomain.toString(v), p)) m;

let prt(m) =
    let rec prtInternal(entryList) =
        match entryList with
        | [] -> ""
        | ((i, j, d,_)::t) -> (i).ToString() + "-(" + d + ")->" + (j).ToString() + ", " + prtInternal(t)
    prtInternal(lstPrt(m))

let I(n:int,pat) = M(List.init n (fun i -> (i+1, i+1, AbstractDomain.copy, pat)));

let rec listsame = function
    | ([],[]) -> true
    | (_,[])  -> false
    | ([],_)  -> false
    | ((i1,j1,v1,_)::t1 as m1, (i2,j2,v2,_)::t2 as m2) ->
        (i1,j1)=(i2,j2) && v1=v2 && listsame(t1,t2)

let same(M m1, M m2) = listsame(m1,m2);

(* listsqcup merges sorted lists *)
let rec listsqcup = function
    | ([],m2) -> m2
    | (m1,[]) -> m1
    | (((i1,j1,v1,p1)::t1 as m1), ((i2,j2,v2,p2)::t2 as m2)) ->
        if (i1,j1)=(i2,j2) then
            let p = match (v1,v2) with
                    | (AbstractDomain.AbstractValue x1, AbstractDomain.AbstractValue x2) ->
                                                Pattern.reduce(if x1 > x2 then p1 else if x2 > x1 then p2 else Pattern.smaller(p1,p2))

            (i1, j1, AbstractDomain.lub v1 v2, p) :: listsqcup(t1,t2)
        elif j1<j2 || (j1=j2 && i1<i2) then (i1,j1,v1,p1) :: listsqcup(t1,m2)
        else (i2,j2,v2,p2) :: listsqcup(m1,t2)

let rec sortLst = function
    | []              -> []
    | [ent]           -> [ent]
    | (e1::(e2::rst)) -> listsqcup([e1], sortLst(e2::rst))

let sqcup(M m1, M m2) = M(listsqcup(sortLst(m1),sortLst(m2)));

let prod(M m1, M m2) =
    M(List.fold
        (fun l1 l2 -> listsqcup(l1,l2))
        []
        (List.map
            (fun ((i1,j1,v,p1)) ->  (* multiply one entry from m1 by whole of m2*)
                List.fold (
                    fun acc (i2,j2,u,p2) ->
                        if j1=i2 then (i1,j2,AbstractDomain.prod(v,u),Pattern.prod(p1,p2))::acc else acc)
                    []
                    m2
                )
            m1
        )
    )

(* lst2mat sorts its input - inefficiently *)
let rec lst2mat = function
    | [] -> M([])
    | [ent] -> M([ent])
    | (e1::(e2::rst)) -> sqcup(M [e1], lst2mat(e2::rst))

(* compute a matrix which is like (I n) except that column j is replaced
    with the provided 'col' *)
let ins_in_I(n,j,col) =
    let ilist = match I(n,Pattern.Cmd(-1)) with
                | M(l) -> l

    M(List.fold
        (fun acc (i,jj,v,p) -> (( if jj=j then col else [(i,jj,v,p)] ) @ acc))
            []
            ilist
        )

let LC(l:int, nonlinear:AbstractDomain.abstractValue ,cmdIdx : int) (M m) =
        M(listsqcup(m, List.choose( fun (i,j,v,p) ->
                        if j=l && i<>l then failwith ("BJK.mat.LC: loop variable X" + j.ToString() + " modified inside loop body.")
                        elif i=j then
                            if v=AbstractDomain.additive then Some (l,j,nonlinear,Pattern.Loop(cmdIdx,p))
                            elif v=AbstractDomain.polynomial then Some (l,j,AbstractDomain.exponentialAtLeast,Pattern.Loop(cmdIdx,p))
                            else None
                        else None) m) )

let ones(M(m)) = List.filter (fun (_,_,d,_) -> AbstractDomain.isLinear d) m;
(* the r(M) function: extract all pairs of One/OnePlus entries *)

let r(m) =
    let ones' = ones(m)
    List.fold
        (fun acc (i,j,d,p1) ->
            acc @ (List.choose
                        (fun (i',j',d,p2) -> if (i'<i || (i'=i && j'<j)) then Some((i,j),(i',j'),p1) else None) ones'
                    )
        )
        []
        ones'

(* get all the variable indices that have an abstract value of 'value' *)
let classiedBy(M matrix, AbstractDomain.AbstractValue value) : (int list) =
        matrix
        |> List.filter (fun (_,_,absValue,_) -> absValue = AbstractDomain.AbstractValue(value))
        |> List.map (fun (_,varIndex,_,_) -> varIndex)

(* classify the variables into "properly bounded" (called SAFE in the paper)
    and the rest.  The Unbounded ones are given first!! *)
let classify(M m, vars, AbstractDomain.AbstractValue value) :(int list)*(int list) =
    List.partition (fun i -> List.exists (fun (_,j,d,_) -> (j=i && d >= AbstractDomain.AbstractValue(value))) m) ([1..vars])